Nuprl Definition : es-dt
11,40
postcript
pdf
es-dt(
l
;
da
)
== compose-fpf((
k
.if isrcv(
k
)
== compose-fpf(
then if eq_lnk(lnk(
k
);
l
) then inl tag(
k
) else inr
fi
== compose-fpf(
else inr
== compose-fpf(
fi );
== compose-fpf(
(
tg
.rcv(
l
,
tg
));
== compose-fpf(
da
)
latex
Definitions
compose-fpf(
a
;
b
;
f
)
,
isrcv(
k
)
,
if
b
then
t
else
f
fi
,
eq_lnk(
a
;
b
)
,
lnk(
k
)
,
inl
x
,
tag(
k
)
,
inr
x
,
,
x
.
A
(
x
)
,
rcv(
l
,
tg
)
FDL editor aliases
es-dt
origin